Section: New Results

Compression of SMT proofs

Participants : Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo.

Integrating an SMT solver in a certified environment such as an LF-style proof assistant requires the solver to output proofs. Unfortunately, those proofs may be quite large, and the overhead of rechecking the proof may account for a significant fraction of the proof time. In previous work, we proposed a technique for reducing the sizes of propositional proofs based on the analysis of resolution graphs, which were justified in an algebra of resolution. Unfortunately, the complexity of these techniques turned out to be prohibitive. In a paper published at CADE 2011 [11] , we give practical algorithms for more restricted compression techniques and validate them on standard benchmarks. Our algorithms significantly improve state-of-the-art proof compression algorithms and achieve better reduction of proof sizes, often by 30%.